package pl.elka.pszt.model.solver;

import java.util.ArrayList;
import java.util.Collections;
import java.util.HashMap;
import java.util.HashSet;
import java.util.Iterator;
import java.util.List;
import java.util.ListIterator;
import java.util.Map;
import java.util.Random;
import java.util.Set;
import java.util.Stack;

import pl.elka.pszt.model.Assigned;
import pl.elka.pszt.model.Clause;
import pl.elka.pszt.model.Knowledge;
import pl.elka.pszt.model.KnowledgeElement;
import pl.elka.pszt.model.argument.Argument;
import pl.elka.pszt.model.argument.Constant;
import pl.elka.pszt.model.argument.Variable;
import pl.elka.pszt.model.literal.Literal;
import pl.elka.pszt.utils.Log;

/**
 * Klasa przeprowadzająca wnioskowanie.
 * 
 * @author Andrzej Makarewicz
 * 
 */
public class Reasoning {
	
	private static final String TAG = Reasoning.class.getSimpleName();
	private static final Random RANDOM = new Random(System.currentTimeMillis());
	
	private Knowledge knowledge;
	private Assigned question;
	private ReasoningListener listener;
	
	/**
	 * 
	 * @param solver
	 *            zainicjaliozowany solver
	 * @param listener
	 *            nasluchuje na zakonczenie wnioskowania
	 * @return obiekt {@link Runnable} w ktorym przeprowadzone bedzie
	 *         wnioskowanie
	 */
	public static Runnable createReasoningRunnable(Knowledge knowledge, Assigned question,
			final ReasoningListener listener) {
		if (knowledge == null || question == null || listener == null) throw new NullPointerException();
		
		return new ReasoningRunnable(knowledge, question, listener);
	}
	
	/**
	 * 
	 * Runnable używającej klasy {@link Reasoning} do wnioskowania.
	 * 
	 */
	public static class ReasoningRunnable implements Runnable {
		
		private static final String TAG = ReasoningRunnable.class.getSimpleName();
		
		private final Knowledge knowledge;
		private final Assigned question;
		private final ReasoningListener listener;
		
		public ReasoningRunnable(Knowledge knowledge, Assigned question, ReasoningListener listener) {
			Log.o(TAG, Log.getCurrentMethodName());
			
			this.knowledge = knowledge;
			this.question = question;
			this.listener = listener;
		}
		
		@Override
		public void run() {
			Log.o(TAG, Log.getCurrentMethodName());
			
			Reasoning reasoning = new Reasoning(knowledge, question, listener);
			reasoning.resolve();
		}
		
	}
	
	/**
	 * 
	 * Listener zakończonego wnioskowania
	 * 
	 */
	public static interface ReasoningListener {
		void onReasoningFinished(boolean success, List<KnowledgeElement> k);
	}
	
	public Reasoning(Knowledge knowledge, Assigned question, ReasoningListener listener) {
		Log.o(TAG, Log.getCurrentMethodName());
		
		this.knowledge = knowledge;
		this.question = question;
		this.listener = listener;
	}
	
	/**
	 * Inicjalizuje pomocnicze zmienne oraz uruchamia rekurencyjną funkcję
	 * wnioskującą. Wynik przekazany jest do listenera.
	 */
	public void resolve() {
		Log.o(TAG, Log.getCurrentMethodName());
		
		
		
		boolean result;
		try {
			Stack<KnowledgeElement> k = new Stack<KnowledgeElement>();
			Set<Assigned> h1 = new HashSet<Assigned>();
			Set<Assigned> h0 = new HashSet<Assigned>();
			
			h0.add(question);
			result = reasoning(k, h1, h0);
			
			listener.onReasoningFinished(result, new ArrayList<KnowledgeElement>(k));
		}
		catch (InterruptedException e) {}
		
	}
	
	/**
	 * Rekurencyjna funkcja wnioskujaca.
	 * 
	 * @param k
	 *            stos klauzul
	 * @param h1
	 *            hipotezy wstepnie potwierdzone
	 * @param h0
	 *            hipotezy niepotwierdzone
	 * @return czy udalo sie potwierdzic zapytanie
	 * @throws InterruptedException
	 */
	private boolean reasoning(Stack<KnowledgeElement> k, Set<Assigned> h1, Set<Assigned> h0)
			throws InterruptedException {
		if (Thread.interrupted()) throw new InterruptedException();
		
		// slow it down a little bit
//		long pom = 1;
//		for(long i = 0; i < 9999; i++){
//			for(long j = 0; j < 9999; j++){
//				pom = i * j * pom;
//			}
//		}
		
		if (h0.isEmpty()) {
			return true;
		}
		// losujemy element z h0 do wstepnego potwierdzenia
		Assigned b = getElement(h0);
		
		// znajdujemy dla niego liste pasujacych klauzul
		List<KnowledgeElement> matchingClausule = knowledge.getMatchingElements(b);
		if (matchingClausule == null || matchingClausule.isEmpty()) {
			return false;
		}
		
		// nadajemy losowa kolejnosc rozpatrywanych klauzul
		if (matchingClausule.size() > 1) {
			Collections.shuffle(matchingClausule);
		}
		
		h1.add(b);
		// preferujemy fakty przy wyborze kolejnej klauzuli do rozpatrzenia
		for (Iterator iterator = matchingClausule.iterator(); iterator.hasNext();) {
			KnowledgeElement knowledgeElement = (KnowledgeElement) iterator.next();
			if (knowledgeElement.isFact()) {
				k.add(knowledgeElement);
				h0.remove(b);
				if (reasoning(k, h1, h0)) {
					return true;
				} else {
					iterator.remove();
				}
				h0.add(b);
				k.remove(knowledgeElement);
			}
		}
		
		// gdy rozpatrzymy wszystkie fakty, sprawdzamy klauzule
		for (Iterator iterator = matchingClausule.iterator(); iterator.hasNext();) {
			Clause clause = (Clause) iterator.next();
			Map<Variable, Constant> assigmentMap = createAssignMap(b, clause.getConclusion());
			Set<Assigned> assigned = createAssignedSet(clause.getConjunction(), assigmentMap);
			if (!areAssignedInSet(h1, assigned)) {
				assigned.removeAll(h0); // nie moga wystapic powtorzenia z h0
				h0.addAll(assigned);
				k.add(clause);
				h0.remove(b);
				if (reasoning(k, h1, h0)) {
					return true;
				}
				h0.add(b);
				k.remove(clause);
				h0.removeAll(assigned);
			}
		}
		h1.remove(b);
		
		return false;
	}
	
	/**
	 * 
	 * @param literals
	 *            zbior literalow do ktorych chcemy przypisac stale
	 * @param assigmentMap
	 *            mapa przypisan zmiennych na stale
	 * @return zbior przypisanych literalow
	 */
	private Set<Assigned> createAssignedSet(Set<Literal> literals, Map<Variable, Constant> assigmentMap) {
		Set<Assigned> ret = new HashSet<>();
		for (Literal l : literals) {
			ret.add(new Assigned(l, assigmentMap));
		}
		return ret;
	}
	
	/**
	 * @param h1Set
	 *            zbior h1 w ktorym sprawdzamy wystapienie
	 * @param assignedSet
	 *            zbior przypisanych
	 * @return czy dowolny element z przypisanych wystepuje w zbiorze h1
	 */
	private boolean areAssignedInSet(Set<Assigned> h1Set, Set<Assigned> assignedSet) {
		for (Iterator iterator = assignedSet.iterator(); iterator.hasNext();) {
			Assigned assigned = (Assigned) iterator.next();
			
			if (h1Set.contains(assigned)) return true;
		}
		return false;
	}
	
	/**
	 * 
	 * @param assigned
	 *            literal z przypisanymi wartosciami stalymi jako argumenty
	 * @param conlusion
	 *            literal do ktorego ma nastapic podstawienie
	 * @return mapa przypisan zmiennych do stalych
	 */
	private Map<Variable, Constant> createAssignMap(Assigned assigned, Literal conlusion) {
		Map<Variable, Constant> ret = new HashMap<Variable, Constant>();
		
		ListIterator<? extends Argument> a = assigned.getArguments().listIterator();
		ListIterator<? extends Argument> c = conlusion.getArguments().listIterator();
		while (a.hasNext() && c.hasNext()) {
			Argument oa = a.next();
			Argument oc = c.next();
			if (oc.isVariable()) {
				ret.put((Variable) oc, (Constant) oa);
			}
		}
		
		return ret;
	}
	
	/**
	 * 
	 * @param set
	 *            zbiór literalow z przypisanymi stalymi
	 * @return losowy element zbioru
	 */
	private Assigned getElement(Set<Assigned> set) {
		Iterator iterator = set.iterator();
		int size = set.size();
		
		if (size > 1) {
			int position = RANDOM.nextInt(size);
			while (position-- > 0) {
				iterator.next();
			}
		}
		
		return (Assigned) iterator.next();
	}
}
